<!DOCTYPE html PUBLIC "-//W3C//DTD HTML 4.01//EN" "http://www.w3.org/TR/html4/strict.dtd">
<html><head>
<meta content="text/html; charset=ISO-8859-1" http-equiv="content-type"><title>help for SAToulouse</title></head>
<body>
<big><big><big><span style="font-weight: bold;">SAToulouse has solved the problem.</span></big></big></big><br><br>Either you have obtained :<br><br><ul><li>"the set of formulas is satisfiable"</li></ul>SAToulouse gives you a model/valuation for it.<br><br>If SAToulouse gives "p, q, r", it means that the valuation v defined by<br>v(p) = v(q) = v(r) = 1 and v(s) = 0 for all propositions s different from p, q and r,<br>is such that v satisfies all the formulas.<br>Intuitively, the valuation v is a solution for the constraints represented by the formulas.<br><br><br>In
the case where there is a lot of propositional variables, you can only
watch the truthness of some propositional variables. You can select a
subset of propositional variables by typing a common portion of the
namesof the propositional variables you want to watch. <br><br><br><ul><li>"the set of formulas is unsatisfable"</li></ul>There
is no valuation v such that v satisfies all the formulas. Generally
speaking, it means that the constraints represented by the formulas can
not be satisfied alltogether.<br><br><br><br><br><br><br><br>
</body></html>